nLab first-order set theory

Idea

A first-order set theory is a set theory which is a first-order theory. These include unsorted set theories like ZFC and fully formal ETCS, simply sorted set theories like the two-sorted presentation of ETCS, and dependently sorted set theories like the usual presentation of ETCS and SEAR.

It contrasts with other approaches to set theory which are not first-order theories, such as set-level type theories like XTT or Martin-Löf type theory with a type of all propositions and UIP/axiom K, all of which could be considered to be set theories.

Related concepts

• predicate logic

• set-level type theory

References

• Steve Awodey, Carsten Butz, Alex Simpson, Thomas Streicher, Relating first-order set theories, toposes and categories of classes, Annals of Pure and Applied Logic 165 2 (2014) 428-502 [doi:10.1016/j.apal.2013.06.004]